Termination of the given ITRSProblem could successfully be proven:



↳ ITRS
  ↳ ITRStoQTRSProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

g(x, cons(y, ys)) → cons(+@z(x, y), g(x, ys))

The set Q consists of the following terms:

g(x0, cons(x1, x2))


Represented integers and predefined function symbols by Terms

↳ ITRS
  ↳ ITRStoQTRSProof
    ↳ QTRS
      ↳ QTRSRRRProof

Q restricted rewrite system:
The TRS R consists of the following rules:

g(x, cons(y, ys)) → cons(plus_int(x, y), g(x, ys))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

g(x0, cons(x1, x2))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))


The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

g(x, cons(y, ys)) → cons(plus_int(x, y), g(x, ys))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

g(x0, cons(x1, x2))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

Used ordering:
Combined order from the following AFS and order.
g(x1, x2)  =  g(x1, x2)
cons(x1, x2)  =  cons(x1, x2)
plus_int(x1, x2)  =  plus_int(x1, x2)
pos(x1)  =  x1
neg(x1)  =  neg(x1)
minus_nat(x1, x2)  =  minus_nat(x1, x2)
plus_nat(x1, x2)  =  plus_nat(x1, x2)
0  =  0
s(x1)  =  s(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
g2 > cons2 > [neg1, 0, s1]
g2 > plusint2 > minusnat2 > [neg1, 0, s1]
g2 > plusint2 > plusnat2 > [neg1, 0, s1]

Status:
cons2: multiset
plusnat2: multiset
g2: [2,1]
neg1: multiset
plusint2: [2,1]
s1: multiset
minusnat2: multiset
0: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

g(x, cons(y, ys)) → cons(plus_int(x, y), g(x, ys))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)




↳ ITRS
  ↳ ITRStoQTRSProof
    ↳ QTRS
      ↳ QTRSRRRProof
        ↳ QTRS
          ↳ RisEmptyProof
          ↳ RisEmptyProof
          ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
The set Q consists of the following terms:

g(x0, cons(x1, x2))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))


The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.